λ(_ : Natural) → _
